i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da).
"ecl"  dom(ds)  ecl-machine1{ecl:ut2}(i; ds; da; A)  Realizer 

latex

Definitions	Id, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), P  Q, x:A. B(x), "$x", x. t(x), t  T, ecl-machine1{$ecl:ut2}(i; ds; da; A), x(s), ecl-trans-tuple{i:l}(ds;da), Prop
Lemmas	fpf-trivial-subtype-top, fpf-dom wf, fpf-compatible-single, ecl-trans-tuple wf, id-deq wf, assert wf, Knd wf, R-state-var-init wf, Id wf, fpf wf, ecl wf, ecl-trans wf, not wf